SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Tree automaton</title>

</head>

Tree automaton

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div role="note" class="hatnote navigation-not-searchable">For a different notion of tree automaton, see <a href="Tree_walking_automaton" class="mw-redirect" title="Tree walking automaton">tree walking automaton</a>.</div>

A tree automaton is a type of <a href="State_machine" class="mw-redirect" title="State machine">state machine</a>. Tree automata deal with <a href="Tree_structure" title="Tree structure">tree structures</a>, rather than the <a href="String_(computer_science)" title="String (computer science)">strings</a> of more conventional state machines.

The following article deals with branching tree automata, which correspond to <a href="Regular_tree_language" class="mw-redirect" title="Regular tree language">regular languages of trees</a>.

As with classical automata, finite tree automata (FTA) can be either a <a href="Deterministic_automaton" title="Deterministic automaton">deterministic automaton</a> or not. According to how the automaton processes the input tree, finite tree automata can be of two types: (a) bottom up, (b) top down. This is an important issue, as although non-deterministic (ND) top-down and ND bottom-up tree automata are equivalent in expressive power, deterministic top-down automata are strictly less powerful than their deterministic bottom-up counterparts, because tree properties specified by deterministic top-down tree automata can only depend on path properties. (Deterministic bottom-up tree automata are as powerful as ND tree automata.)

<div class="mw-heading mw-heading2"><h2 id="Definitions">Definitions</h2></div>

A bottom-up finite tree automaton over F is defined as a tuple

(Q, F, Qf, Δ),

where Q is a set of states, F is a <a href="Ranked_alphabet" title="Ranked alphabet">ranked alphabet</a> (i.e., an alphabet whose symbols have an associated <a href="Arity" title="Arity">arity</a>), Qf ⊆ Q is a set of final states, and Δ is a set of <a href="Production_(computer_science)" title="Production (computer science)">transition rules</a> of the form f(q1(x1),...,qn(xn)) → q(f(x1,...,xn)), for an n-ary f ∈ F, q, qi ∈ Q, and xi variables denoting subtrees. That is, members of Δ are rewrite rules from nodes whose childs' roots are states, to nodes whose roots are states. Thus the state of a node is deduced from the states of its children.

For n=0, that is, for a constant symbol f, the above transition rule definition reads f() → q(f()); often the empty parentheses are omitted for convenience: f → q(f).

Since these transition rules for constant symbols (leaves) do not require a state, no explicitly defined initial states are needed.

A bottom-up tree automaton is run on a <a href="Ground_term" class="mw-redirect" title="Ground term">ground term</a> over F, starting at all its leaves simultaneously and moving upwards, associating a run state from Q with each subterm.

The term is accepted if its root is associated to an accepting state from Qf.<a href="#cite_note-FOOTNOTEComon_et_al.2008sect._1.1,_p._20-1">[1]</a>

A top-down finite tree automaton over F is defined as a tuple

(Q, F, Qi, Δ),

with two differences with bottom-up tree automata. First, Qi ⊆ Q, the set of its initial states, replaces Qf; second, its transition rules are oriented conversely:

q(f(x1,...,xn)) → f(q1(x1),...,qn(xn)), for an n-ary f ∈ F, q, qi ∈ Q, and xi variables denoting subtrees.

That is, members of Δ are here rewrite rules from nodes whose roots are states to nodes whose children's roots are states.

A top-down automaton starts in some of its initial states at the root and moves downward along branches of the tree, associating along a run a state with each subterm inductively.

A tree is accepted if every branch can be gone through this way.<a href="#cite_note-FOOTNOTEComon_et_al.2008sect._1.6,_p._38-2">[2]</a>

A tree automaton is called deterministic (abbreviated DFTA) if no two rules from Δ have the same left hand side; otherwise it is called nondeterministic (NFTA).<a href="#cite_note-FOOTNOTEComon_et_al.2008sect._1.1,_p._23-3">[3]</a> Non-deterministic top-down tree automata have the same expressive power as non-deterministic bottom-up ones;<a href="#cite_note-FOOTNOTEComon_et_al.2008sect._1.6,_theorem_1.6.1,_p._38-4">[4]</a> the transition rules are simply reversed, and the final states become the initial states.

In contrast, deterministic top-down tree automata<a href="#cite_note-5">[5]</a> are less powerful than their bottom-up counterparts, because in a deterministic tree automaton no two transition rules have the same left-hand side. For tree automata, transition rules are rewrite rules; and for top-down ones, the left-hand side will be parent nodes. Consequently, a deterministic top-down tree automaton will only be able to test for tree properties that are true in all branches, because the choice of the state to write into each child branch is determined at the parent node, without knowing the child branches contents. For example, if F consists of f, g, and a, which are 2ary, 1ary, and 0ary, respectively, the set of all terms having a ground instance of f(a,g(x)) as a subterm, can be recognized by a bottom-up DFTA, but not by a top-town DFTA.<a href="#cite_note-6">[a]</a><a href="#cite_note-FOOTNOTEComon_et_al.2008sect._1.8,_exercise_1.2_and_1.6.3,_p.43-44-7">[6]</a>

<a href="Infinite-tree_automaton" title="Infinite-tree automaton">Infinite-tree automata</a> extend top-down automata to infinite trees, and can be used to prove decidability of <a href="S2S_(mathematics)" title="S2S (mathematics)"> S2S</a>, the <a href="Monadic_second-order_logic" title="Monadic second-order logic"> monadic second-order</a> theory with two successors. Finite tree automata (nondeterministic if top-down) suffice for WS2S.<a href="#cite_note-8">[7]</a>

<div class="mw-heading mw-heading2"><h2 id="Examples">Examples</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Bottom-up_automaton_accepting_boolean_lists">Bottom-up automaton accepting boolean lists</h3></div>

Employing coloring to distinguish members of F and Q, and using the ranked alphabet F={ <style data-mw-deduplicate="TemplateStyles:r1239334494">

/* start https://en.wikipedia.org/ */

@media screen{html.skin-theme-clientpref-night .mw-parser-output div:not(.notheme)>.tmp-color,html.skin-theme-clientpref-night .mw-parser-output p>.tmp-color,html.skin-theme-clientpref-night .mw-parser-output table:not(.notheme) .tmp-color{color:inherit!important}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output div:not(.notheme)>.tmp-color,html.skin-theme-clientpref-os .mw-parser-output p>.tmp-color,html.skin-theme-clientpref-os .mw-parser-output table:not(.notheme) .tmp-color{color:inherit!important}}

/* end https://en.wikipedia.org/ */

</style>false,true,nil,cons(.,.) }, with cons having arity 2 and all other symbols having arity 0, a bottom-up tree automaton accepting the set of all finite lists of boolean values can be defined as (Q, F, Qf, Δ) with Q = { Bool,BList }, Qf = { BList }, and Δ consisting of the rules

<td>false</td>

<td>Bool(false)</td>

<td>(1),

</td></tr>

<tr>

<td>(2),

</td></tr>

<tr>

<td>BList(nil)</td>

<td>(3), and

</td></tr>

<tr>

<td>cons(Bool(x1),BList(x2))</td>

<td>BList(cons(x1,x2))      </td>

<td>(4).

</td></tr></tbody></table></dd></dl>

In this example, the rules can be understood intuitively as assigning to each term its type in a bottom-up manner; e.g. rule (4) can be read as "A term cons(x1,x2) has type BList, provided x1 and x2 has type Bool and BList, respectively".

An accepting example run is

<td>

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">false,

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">true,

</td>

<td align="RIGHT">nil

</td>

<td>))

</td></tr>

<tr>

<td>⇒

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">false,

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">true,

</td>

<td align="RIGHT">BList(nil)

</td>

<td>))

</td>

<td>by (3)

</td></tr>

<tr>

<td>⇒

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">false,

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">Bool(true),

</td>

<td align="RIGHT">BList(nil)

</td>

<td>))

</td>

<td>by (2)

</td></tr>

<tr>

<td>⇒

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">false,

</td>

<td align="RIGHT">BList(cons(

</td>

<td align="RIGHT">true,

</td>

<td align="RIGHT">nil

</td>

<td>)))

</td>

<td>by (4)

</td></tr>

<tr>

<td>⇒

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">Bool(false),

</td>

<td align="RIGHT">BList(cons(

</td>

<td align="RIGHT">true,

</td>

<td align="RIGHT">nil

</td>

<td>)))

</td>

<td>by (1)

</td></tr>

<tr>

<td>⇒

</td>

<td align="RIGHT">BList(cons(

</td>

<td align="RIGHT">false,

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">true,

</td>

<td align="RIGHT">nil

</td>

<td>)))

</td>

<td>by (4), accepted.

</td></tr></tbody></table></dd></dl>

Cf. the derivation of the same term from a regular tree grammar corresponding to the automaton, shown at <a href="Regular_tree_grammar#Examples" title="Regular tree grammar">Regular tree grammar#Examples</a>.

A rejecting example run is

<td>

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">false,

</td>

<td align="RIGHT">true

</td>

<td>)

</td></tr>

<tr>

<td>⇒

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">false,

</td>

<td align="RIGHT">Bool(true)

</td>

<td>)

</td>

<td>by (1)

</td></tr>

<tr>

<td>⇒

</td>

<td align="RIGHT">cons(

</td>

<td align="RIGHT">Bool(false),

</td>

<td align="RIGHT">Bool(true)

</td>

<td>)

</td>

<td>by (2), no further rule applicable.

</td></tr></tbody></table></dd></dl>

Intuitively, this corresponds to the term cons(false,true) not being well-typed.

<div class="mw-heading mw-heading3"><h3 id="Top-down_automaton_accepting_multiples_of_3_in_binary_notation">Top-down automaton accepting multiples of 3 in binary notation</h3></div>

<th>

</th>

<th align="center">(A)

</th>

<th align="center">(B)

</th>

<th align="center">(C)

</th>

<th align="center">(D)

</th></tr>

<tr>

<th>

</th>

<th align="center"><a href="Regular_grammar#Strictly_regular_grammars" title="Regular grammar">String grammar</a> rules

</th>

<th align="center"><a href="Deterministic_finite_automaton#Formal_definition" title="Deterministic finite automaton">String automaton</a> transitions

</th>

<th align="center">Tree automaton transitions

</th>

<th align="center"><a href="Regular_tree_grammar#Definition" title="Regular tree grammar">Tree grammar</a> rules

</th></tr>

<tr>

<td>

<table>

<th>0

</th></tr>

<tr>

<th>1

</th></tr>

<tr>

<th>2

</th></tr>

<tr>

<th>3

</th></tr>

<tr>

<th>4

</th></tr>

<tr>

<th>5

</th></tr>

<tr>

<th>6

</th></tr></tbody></table>

</td>

<td>

<table>

<td>ε

</td></tr>

<tr>

<td>0 S0

</td></tr>

<tr>

<td>1 S1

</td></tr>

<tr>

<td>0 S2

</td></tr>

<tr>

<td>1 S0

</td></tr>

<tr>

<td>0 S1

</td></tr>

<tr>

<td>1 S2

</td></tr></tbody></table>

</td>

<td>

<table>

<td>

</td></tr>

<tr>

<td>= S0

</td></tr>

<tr>

<td>= S1

</td></tr>

<tr>

<td>= S2

</td></tr>

<tr>

<td>= S0

</td></tr>

<tr>

<td>= S1

</td></tr>

<tr>

<td>= S2

</td></tr></tbody></table>

</td>

<td>

<table>

<td>nil

</td></tr>

<tr>

<td>0(S0(x))

</td></tr>

<tr>

<td>1(S1(x))

</td></tr>

<tr>

<td>0(S2(x))

</td></tr>

<tr>

<td>1(S0(x))

</td></tr>

<tr>

<td>0(S1(x))

</td></tr>

<tr>

<td>1(S2(x))

</td></tr></tbody></table>

</td>

<td>

<table>

<td>nil

</td></tr>

<tr>

<td>0(S0)

</td></tr>

<tr>

<td>1(S1)

</td></tr>

<tr>

<td>0(S2)

</td></tr>

<tr>

<td>1(S0)

</td></tr>

<tr>

<td>0(S1)

</td></tr>

<tr>

<td>1(S2)

</td></tr></tbody></table>

<td>

</td></tr></tbody></table>

Using the same colorization as above, this example shows how tree automata generalize ordinary string automata.

The finite deterministic string automaton shown in the picture accepts all strings of binary digits that denote a multiple of 3.

Using the notions from <a href="Deterministic_finite_automaton#Formal_definition" title="Deterministic finite automaton">Deterministic finite automaton#Formal definition</a>, it is defined by:

<ul><li>the set Q of states being { S0, S1, S2 },</li>

<li>the input alphabet being { 0, 1 },</li>

<li>the initial state being S0,</li>

<li>the set of final states being { S0 }, and</li>

<li>the transitions being as shown in column (B) of the table.</li></ul>

In the tree automaton setting, the input alphabet is changed such that the symbols 0 and 1 are both unary, and a nullary symbol, say nil is used for tree leaves.

For example, the binary string "110" in the string automaton setting corresponds to the term "1(1(0(nil)))" in the tree automaton setting; this way, strings can be generalized to trees, or terms.

The top-down finite tree automaton accepting the set of all terms corresponding to multiples of 3 in binary string notation is then defined by:

<ul><li>the set Q of states being still { S0, S1, S2 },</li>

<li>the ranked input alphabet being { 0, 1, nil }, with Arity(0)=Arity(1)=1 and Arity(nil)=0, as explained,</li>

<li>the set of initial states being { S0 }, and</li>

<li>the transitions being as shown in column (C) of the table.</li></ul>

For example, the tree "1(1(0(nil)))" is accepted by the following tree automaton run:

<table>

<td>))))

</td></tr>

<tr>

<td>by 2

</td></tr>

<tr>

<td>by 4

</td></tr>

<tr>

<td>by 1

</td></tr>

<tr>

<td>by 0

</td></tr></tbody></table>

In contrast, the term "1(0(nil))" leads to following non-accepting automaton run:

<table>

<td>)))

</td></tr>

<tr>

<td>by 2

</td></tr>

<tr>

<td>by 3, no further rule applicable

</td></tr></tbody></table>

Since there are no other initial states than S0 to start an automaton run with, the term "1(0(nil))" is not accepted by the tree automaton.

For comparison purposes, the table gives in column (A) and (D) a <a href="Regular_grammar#Strictly_regular_grammars" title="Regular grammar">(right) regular (string) grammar</a>, and a <a href="Regular_tree_grammar#Definition" title="Regular tree grammar">regular tree grammar</a>, respectively, each accepting the same language as its automaton counterpart.

<div class="mw-heading mw-heading2"><h2 id="Properties">Properties</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Recognizability">Recognizability</h3></div>

For a bottom-up automaton, a ground term t (that is, a tree) is accepted if there exists a reduction that starts from t and ends with q(t), where q is a final state. For a top-down automaton, a ground term t is accepted if there exists a reduction that starts from q(t) and ends with t, where q is an initial state.

The tree language L(A) accepted, or recognized, by a tree automaton A is the set of all ground terms accepted by A. A set of ground terms is recognizable if there exists a tree automaton that accepts it.

A linear (that is, arity-preserving) tree homomorphism preserves recognizability.<a href="#cite_note-9">[8]</a>

<div class="mw-heading mw-heading3"><h3 id="Completeness_and_reduction">Completeness and reduction</h3></div>

A non-deterministic finite tree automaton is complete if there is at least one transition rule available for every possible symbol-states combination.

A state q is accessible if there exists a ground term t such that there exists a reduction from t to q(t).

An NFTA is reduced if all its states are accessible.<a href="#cite_note-FOOTNOTEComon_et_al.2008sect._1.1,_p._23-24-10">[9]</a>

<div class="mw-heading mw-heading3"><h3 id="Pumping_lemma">Pumping lemma</h3></div>

Every sufficiently large<a href="#cite_note-11">[10]</a> ground term t in a recognizable tree language L can be vertically tripartited<a href="#cite_note-12">[11]</a> such that arbitrary repetition ("pumping") of the middle part keeps the resulting term in L.<a href="#cite_note-13">[12]</a><a href="#cite_note-FOOTNOTEComon_et_al.2008sect._1.2,_p._29-14">[13]</a>

For the language of all finite lists of boolean values from the above example, all terms beyond the height limit k=2 can be pumped, since they need to contain an occurrence of cons. For example,

<td>cons(false,

</td>

<td>cons(true,nil)

</td>

<td>)

</td>

<td>,

</td></tr>

<tr>

</td>

<td>cons(true,nil)

</td>

<td>))

</td>

<td>,

</td></tr>

<tr>

<td>cons(false,cons(false,cons(false,

</td>

<td>cons(true,nil)

</td>

<td>)))

</td>

<td>, ...

</td></tr></tbody></table></dd></dl>

all belong to that language.

<div class="mw-heading mw-heading3"><h3 id="Closure">Closure</h3></div>

The class of recognizable tree languages is closed under union, under complementation, and under intersection.<a href="#cite_note-FOOTNOTEComon_et_al.2008sect._1.3,_theorem_1.3.1,_p._30-15">[14]</a>

<div class="mw-heading mw-heading3"><h3 id="Myhill–Nerode_theorem">Myhill–Nerode theorem</h3></div>

A congruence on the set of all trees over a ranked alphabet F is an <a href="Equivalence_relation" title="Equivalence relation">equivalence relation</a> such that u1 ≡ v1 and ... and un ≡ vn implies f(u1,...,un) ≡ f(v1,...,vn), for every f ∈ F.

It is of finite index if its number of equivalence-classes is finite.

For a given tree-language L, a congruence can be defined by u ≡L v if C[u] ∈ L ⇔ C[v] ∈ L for each context C.

The <a href="Myhill%E2%80%93Nerode_theorem" title="Myhill–Nerode theorem">Myhill–Nerode theorem</a> for tree automata states that the following three statements are equivalent:<a href="#cite_note-FOOTNOTEComon_et_al.2008sect._1.5,_p_.36-16">[15]</a>

<ol><li>L is a recognizable tree language</li>

<li>L is the union of some equivalence classes of a congruence of finite index</li>

<li>the relation ≡L is a congruence of finite index</li></ol>

<div class="mw-heading mw-heading2"><h2 id="History">History</h2></div>

According to Engelfriet,<a href="#cite_note-FOOTNOTEEngelfriet1975-17">[16]</a> bottom-up finite tree automata were invented around 1965 independently by (<a href="#CITEREFDoner1965">Doner 1965</a>)

(<a href="#CITEREFDoner1970">Doner 1970</a>) and (<a href="#CITEREFThatcherWright1968">Thatcher & Wright 1968</a>), and somewhat later by (<a href="#CITEREFPairQuere1968">Pair & Quere 1968</a>);

top-down finite tree automata were introduced by (<a href="#CITEREFRabin1969">Rabin 1969</a>) and (<a href="#CITEREFMagidorMoran1969">Magidor & Moran 1969</a>), and regular tree grammars by (<a href="#CITEREFBrainerd1969">Brainerd 1969</a>).

In the November 1965 issue of <a href="Notices_of_the_ACM" class="mw-redirect" title="Notices of the ACM">Notices of the ACM</a>, two abstracts (<a href="#CITEREFDoner1965">Doner 1965</a>) and (<a href="#CITEREFThatcherWright1965">Thatcher & Wright 1965</a>) were presented, both received on September 17. Both abstracts refer to each other, saying that finite tree automata have been discovered independently, while Thatcher & Wright admit that their application to prove decidability of "the weak second-order theory of k successor functions" was first obtained by Doner.

<ul><li><a href="Courcelle's_theorem" title="Courcelle's theorem">Courcelle's theorem</a> - an application of tree automata to prove an algorithmic meta-theorem about graphs</li>

<li><a href="Tree_transducers" class="mw-redirect" title="Tree transducers">Tree transducers</a> - extend tree automata in the same way that <a href="Finite-state_transducer" title="Finite-state transducer">word transducers</a> extend <a href="Finite-state_automata" class="mw-redirect" title="Finite-state automata">word automata</a>.</li>

<li><a href="Alternating_tree_automata" title="Alternating tree automata">Alternating tree automata</a></li>

<li><a href="Infinite-tree_automaton" title="Infinite-tree automaton">Infinite-tree automata</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Notes">Notes</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

<li id="cite_note-FOOTNOTEComon_et_al.2008sect._1.1,_p._20-1"><a href="#cite_ref-FOOTNOTEComon_et_al.2008sect._1.1,_p._20_1-0">^</a> <a href="#CITEREFComon_et_al.2008">Comon et al. 2008</a>, sect. 1.1, p. 20.

</li>

<li id="cite_note-FOOTNOTEComon_et_al.2008sect._1.6,_p._38-2"><a href="#cite_ref-FOOTNOTEComon_et_al.2008sect._1.6,_p._38_2-0">^</a> <a href="#CITEREFComon_et_al.2008">Comon et al. 2008</a>, sect. 1.6, p. 38.

</li>

<li id="cite_note-FOOTNOTEComon_et_al.2008sect._1.1,_p._23-3"><a href="#cite_ref-FOOTNOTEComon_et_al.2008sect._1.1,_p._23_3-0">^</a> <a href="#CITEREFComon_et_al.2008">Comon et al. 2008</a>, sect. 1.1, p. 23.

</li>

<li id="cite_note-FOOTNOTEComon_et_al.2008sect._1.6,_theorem_1.6.1,_p._38-4"><a href="#cite_ref-FOOTNOTEComon_et_al.2008sect._1.6,_theorem_1.6.1,_p._38_4-0">^</a> <a href="#CITEREFComon_et_al.2008">Comon et al. 2008</a>, sect. 1.6, theorem 1.6.1, p. 38.

</li>

<li id="cite_note-5"><a href="#cite_ref-5">^</a> In a strict sense, deterministic top-down automata are not defined by <a href="#CITEREFComon_et_al.2008">Comon et al. (2008)</a> but they are used there (sect. 1.6, proposition 1.6.2, p. 38). They accept the class of path-closed tree languages (sect. 1.8, exercise 1.6, p. 43-44).

</li>

<li id="cite_note-FOOTNOTEComon_et_al.2008sect._1.8,_exercise_1.2_and_1.6.3,_p.43-44-7"><a href="#cite_ref-FOOTNOTEComon_et_al.2008sect._1.8,_exercise_1.2_and_1.6.3,_p.43-44_7-0">^</a> <a href="#CITEREFComon_et_al.2008">Comon et al. 2008</a>, sect. 1.8, exercise 1.2 and 1.6.3, p.43-44.

</li>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFMorawietzCornell1997" class="citation book cs1">Morawietz, Frank; Cornell, Tom (1997-07-07). <a rel="nofollow" class="external text" href="https://dl.acm.org/doi/10.3115/976909.979677">"Representing constraints with automata"</a>. Proceedings of the 35th annual meeting on Association for Computational Linguistics -. ACL '98/EACL '98. USA: Association for Computational Linguistics. pp. 468–475. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.3115%2F976909.979677">10.3115/976909.979677</a>.</cite>

</li>

<li id="cite_note-9"><a href="#cite_ref-9">^</a> The notion in <a href="#CITEREFComon_et_al.2008">Comon et al. (2008</a>, sect. 1.4, theorem 1.4.3, p. 31-32) of tree homomorphism is more general than that of the article "tree homomorphism".

</li>

<li id="cite_note-FOOTNOTEComon_et_al.2008sect._1.1,_p._23-24-10"><a href="#cite_ref-FOOTNOTEComon_et_al.2008sect._1.1,_p._23-24_10-0">^</a> <a href="#CITEREFComon_et_al.2008">Comon et al. 2008</a>, sect. 1.1, p. 23-24.

</li>

<li id="cite_note-11"><a href="#cite_ref-11">^</a> Formally: <a href="Term_(logic)#Operations_with_terms" title="Term (logic)">height</a>(t) > k, with k > 0 depending only on L, not on t

</li>

<li id="cite_note-12"><a href="#cite_ref-12">^</a> Formally: there is a context C[.], a nontrivial context C′[.], and a ground term u such that t = C[C′[u]]. A "context" C[.] is a tree with one hole (or, correspondingly, a term with one occurrence of one variable). A context is called "trivial" if the tree consists only of the hole node (or, correspondingly, if the term is just the variable). The notation C[t] means the result of inserting the tree t into the hole of C[.] (or, correspondingly, <a href="Ground_instance" class="mw-redirect" title="Ground instance">instantiating</a> the variable to t). <a href="#CITEREFComon_et_al.2008">Comon et al. 2008</a>, p. 17, gives a formal definition.

</li>

<li id="cite_note-13"><a href="#cite_ref-13">^</a> Formally: C[C′n[u]] ∈ L for all n ≥ 0. The notation Cn[.] means the result of stacking n copies of C[.] one in another, cf. <a href="#CITEREFComon_et_al.2008">Comon et al. 2008</a>, p. 17.

</li>

<li id="cite_note-FOOTNOTEComon_et_al.2008sect._1.2,_p._29-14"><a href="#cite_ref-FOOTNOTEComon_et_al.2008sect._1.2,_p._29_14-0">^</a> <a href="#CITEREFComon_et_al.2008">Comon et al. 2008</a>, sect. 1.2, p. 29.

</li>

<li id="cite_note-FOOTNOTEComon_et_al.2008sect._1.3,_theorem_1.3.1,_p._30-15"><a href="#cite_ref-FOOTNOTEComon_et_al.2008sect._1.3,_theorem_1.3.1,_p._30_15-0">^</a> <a href="#CITEREFComon_et_al.2008">Comon et al. 2008</a>, sect. 1.3, theorem 1.3.1, p. 30.

</li>

<li id="cite_note-FOOTNOTEComon_et_al.2008sect._1.5,_p_.36-16"><a href="#cite_ref-FOOTNOTEComon_et_al.2008sect._1.5,_p_.36_16-0">^</a> <a href="#CITEREFComon_et_al.2008">Comon et al. 2008</a>, sect. 1.5, p .36.

</li>

<li id="cite_note-FOOTNOTEEngelfriet1975-17"><a href="#cite_ref-FOOTNOTEEngelfriet1975_17-0">^</a> <a href="#CITEREFEngelfriet1975">Engelfriet 1975</a>.

</li>

</ol></div></div>

<li id="cite_note-6"><a href="#cite_ref-6">^</a> Let Q = { qa, qg, qf, q0 }, with the informal meaning qa: "saw an a", qg: "saw some g(...)", qf: saw some f(a,g(...))", q0: "saw none of those". Let Qf = { qf } be the set of final states. The transition rules set Δ =

{

a → qa(a),

f(qa(x),qg(y)) → qf(f(x,y))

} ∪ {

g(qf(x)) → qf(g(x))

} ∪ {

f(qf(x),q(y)) → qf(f(x,y)),

f(q(x),qf(y)) → qf(f(x,y)),

: q ∈ Q

} ∪ {

g(q(x)) → qg(g(x)),

: q ∈ Q \ { qf }

} ∪ {

f(qg(x),q(y)) → q0(f(x,y)),

f(q(x),qa(y)) → q0(f(x,y))

: q ∈ Q

}

maintains the informal meanings of the states during bottom-up movement through a tree t and hence accepts t if, and only if, t somewhere contains a subtree f(a,g(...)).

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

<ul><li><cite id="CITEREFBrainerd1967" class="citation thesis cs1">Brainerd, Walter Scott (Jun 1967). <a rel="nofollow" class="external text" href="https://www.proquest.com/openview/d7dcd98ad551129a997e2b89e01aa538/1?pq-origsite=gscholar&cbl=18750&diss=y">Tree generating systems and tree automata</a> (Ph.D. thesis). Purdue University.</cite></li>

<li><cite id="CITEREFBrainerd1968" class="citation journal cs1">Brainerd, Walter Scott (1968). <a rel="nofollow" class="external text" href="http://www.sciencedirect.com/science/article/pii/S0019995868909170/pdf?md5=8cad8f4a7cb8a779f2b9611a80b8ef21&pid=1-s2.0-S0019995868909170-main.pdf">"The Minimalization of Tree Automata"</a> (PDF). Information and Control. 13: 484–491.</cite></li>

<li><cite id="CITEREFBrainerd1969" class="citation journal cs1">Brainerd, Walter Scott (Feb 1969). <a rel="nofollow" class="external text" href="https://www.sciencedirect.com/science/article/pii/S0019995869900655">"Tree Generating Regular Systems"</a>. Information and Control. 14 (2): 217–231.</cite></li></ul>

<ul><li><cite id="CITEREFComon_et_al.2008" class="citation book cs1">Comon, Hubert; Dauchet, Max; Gilleron, Rémi; Jacquemard, Florent; Lugiez, Denis; Löding, Christof; Tison, Sophie; Tommasi, Marc (November 2008). <a rel="nofollow" class="external text" href="https://hal.inria.fr/hal-03367725/document">Tree Automata Techniques and Applications</a>. Retrieved 11 February 2014.</cite></li></ul>

<ul><li><cite id="CITEREFDoner1965" class="citation journal cs1">Doner, John (Nov 1965). <a rel="nofollow" class="external text" href="https://www.ams.org/cgi-bin/notices/nxgnotices.pl?fm=main&current=196511">"Decidability of the weak second-order theory of two successors (abstract)"</a>. Notices of the ACM. 12 (7): 819.</cite> Received by AMS: 17 Sep</li>

<li><cite id="CITEREFDoner1967" class="citation report cs1">Doner, John (Jul 1967). <a rel="nofollow" class="external text" href="https://apps.dtic.mil/sti/pdfs/AD0701753.pdf">Tree Acceptors and Some of Their Applications</a> (PDF) (Scientific Report). Air Force Office of Scientific Research.</cite></li>

<li><cite id="CITEREFDoner1970" class="citation journal cs1">Doner, John (Oct 1970). <a rel="nofollow" class="external text" href="https://www.sciencedirect.com/science/article/pii/S0022000070800411">"Tree Acceptors and Some of Their Applications"</a>. Journal of Computer and System Sciences. 4 (5): 406–451.</cite></li></ul>

<ul><li><cite id="CITEREFEngelfriet1975" class="citation arxiv cs1">Engelfriet, Joost (1975). "Tree Automata and Tree Grammars". <a href="ArXiv_(identifier)" class="mw-redirect" title="ArXiv (identifier)">arXiv</a>:<a rel="nofollow" class="external text" href="https://arxiv.org/abs/1510.02036">1510.02036</a> [<a rel="nofollow" class="external text" href="https://arxiv.org/archive/cs.FL">cs.FL</a>].</cite></li></ul>

<ul><li><cite id="CITEREFGécsegSteinby1984" class="citation arxiv cs1">Gécseg, Ferenc; Steinby, Magnus (1984). "Tree Automata". <a href="ArXiv_(identifier)" class="mw-redirect" title="ArXiv (identifier)">arXiv</a>:<a rel="nofollow" class="external text" href="https://arxiv.org/abs/1509.06233">1509.06233</a> [<a rel="nofollow" class="external text" href="https://arxiv.org/archive/cs.FL">cs.FL</a>].</cite></li></ul>

<ul><li><cite id="CITEREFHosoya2010" class="citation book cs1">Hosoya, Haruo (4 November 2010). Foundations of XML Processing: The Tree-Automata Approach. Cambridge University Press. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-139-49236-2</bdi>.</cite></li></ul>

<ul><li><cite id="CITEREFMagidorMoran1969" class="citation report cs1">Magidor, Menachem; Moran, Gadi (1969). Finite Automata over Finite Trees (Technical Report). Hebrew University, Jerusalem.</cite></li></ul>

<ul><li><cite id="CITEREFPairQuere1968" class="citation journal cs1">Pair, C.; Quere, A. (Dec 1968). <a rel="nofollow" class="external text" href="https://www.sciencedirect.com/science/article/pii/S0019995868909996">"Définition et etude des Bilangages réguliers"</a>. Information and Control. 13 (6): 565–593.</cite></li></ul>

<ul><li><cite id="CITEREFRabin1969" class="citation journal cs1">Rabin, M.O. (1969). <a rel="nofollow" class="external text" href="https://www.ams.org/journals/tran/1969-141-00/S0002-9947-1969-0246760-1/S0002-9947-1969-0246760-1.pdf">"Decidability of Second-Order Theories and Automata on Infinite Trees"</a> (PDF). Transactions of the Am. Math. Soc. 141: 1–35. <a href="JSTOR_(identifier)" class="mw-redirect" title="JSTOR (identifier)">JSTOR</a> <a rel="nofollow" class="external text" href="https://www.jstor.org/stable/1995086">1995086</a>.</cite></li></ul>

<ul><li><cite id="CITEREFThatcher1967" class="citation report cs1">Thatcher, J.W. (1967). Characterizing Derivation Trees of Context-Free Grammars through Generalized Finite Automata Theory (Research Note). IBM. NC 719.</cite></li>

<li><cite id="CITEREFThatcher1967" class="citation journal cs1">Thatcher, J.W. (Dec 1967). <a rel="nofollow" class="external text" href="https://www.sciencedirect.com/science/article/pii/S0022000067800229">"Characterizing Derivation Trees of Context-Free Grammars through a Generalization of Finite Automata Theory"</a>. Journal of Computer and System Sciences. 1 (4): 317–322.</cite></li>

<li><cite id="CITEREFThatcherWright1965" class="citation journal cs1">Thatcher, J.W.; Wright, J.B. (Nov 1965). <a rel="nofollow" class="external text" href="https://www.ams.org/cgi-bin/notices/nxgnotices.pl?fm=main&current=196511">"Generalized finite automata (abstract 65T-469)"</a>. Notices of the ACM. 12 (7): 820.</cite> Received by AMS: 17 Sep</li>

<li><cite id="CITEREFThatcherWright1966" class="citation report cs1">Thatcher, J.W.; Wright, J.B. (1966). Generalized Finite Automata Theory with an Application to a Decision Problem of Second-Order Logic (Research Paper). IBM. RC-1713.</cite></li>

<li><cite id="CITEREFThatcherWright1968" class="citation journal cs1">Thatcher, J.W.; Wright, J.B. (1968). "Generalized Finite Automata Theory with an Application to a Decision Problem of Second-Order Logic". Mathematical Systems Theory. 2 (1).</cite></li></ul>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Implementations">Implementations</h3></div>

<ul><li><a rel="nofollow" class="external text" href="http://www.grappa.univ-lille3.fr/~filiot/tata/">Grappa</a> (<a rel="nofollow" class="external text" href="https://web.archive.org/web/20190201065525/http://www.grappa.univ-lille3.fr/~filiot/tata/">Archived</a> February 1, 2019, at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a>) - ranked and unranked tree automata libraries (OCaml)</li>

<li><a rel="nofollow" class="external text" href="https://people.irisa.fr/Thomas.Genet/timbuk">Timbuk</a> - tools for reachability analysis and tree automata calculations (OCaml)</li>

<li><a rel="nofollow" class="external text" href="https://lethal.sourceforge.net/">LETHAL</a> - library for working with finite tree and hedge automata (Java)</li>

<li><a rel="nofollow" class="external text" href="https://www.isa-afp.org/entries/Tree-Automata.html">Machine-checked tree automata library</a> (Isabelle [OCaml, SML, Haskell])</li>

<li><a rel="nofollow" class="external text" href="http://www.fit.vutbr.cz/research/groups/verifit/tools/libvata/">VATA</a> - a library for efficient manipulation of non-deterministic tree automata (C++)</li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1126788409">

/* start https://en.wikipedia.org/ */

.mw-parser-output .plainlist ol,.mw-parser-output .plainlist ul{line-height:inherit;list-style:none;margin:0;padding:0}.mw-parser-output .plainlist ol li,.mw-parser-output .plainlist ul li{margin-bottom:0}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="Automata_theory:_formal_languages_and_formal_grammars385" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div id="Automata_theory:_formal_languages_and_formal_grammars385" style="font-size:114%;margin:0 4em"><a href="Automata_theory" title="Automata theory">Automata theory</a>: <a href="Formal_language" title="Formal language">formal languages</a> and <a href="Formal_grammar" title="Formal grammar">formal grammars</a></div></th></tr><tr><td colspan="2" class="navbox-list navbox-odd plainlist" style="width:100%;padding:0;background:transparent;color:inherit;"><div style="padding:0px"><table class="navbox-columns-table" style="border-spacing: 0px; text-align:left;width:100%;"><tbody><tr><td class="navbox-abovebelow" style="font-weight:bold;"><a href="Chomsky_hierarchy" title="Chomsky hierarchy">Chomsky hierarchy</a></td><td class="navbox-abovebelow" style="border-left:2px solid #fdfdfd;font-weight:bold;"><a href="Formal_grammar" title="Formal grammar">Grammars</a></td><td class="navbox-abovebelow" style="border-left:2px solid #fdfdfd;font-weight:bold;"><a href="Formal_language" title="Formal language">Languages</a></td><td class="navbox-abovebelow" style="border-left:2px solid #fdfdfd;font-weight:bold;"><a href="Abstract_machine" title="Abstract machine">Abstract machines</a></td></tr><tr style="vertical-align:top"><td class="navbox-list" style="padding:0px;text-align: center;width:10em;"><div>

</div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;width:10em;"><div>

<ul><li><a href="Unrestricted_grammar" title="Unrestricted grammar">Unrestricted</a></li>

<li>(no common name)</li>

<li><a href="Context-sensitive_grammar" title="Context-sensitive grammar">Context-sensitive</a></li>

<li>Positive <a href="Range_concatenation_grammars" class="mw-redirect" title="Range concatenation grammars">range concatenation</a></li>

<li><a href="Indexed_grammar" title="Indexed grammar">Indexed</a></li>

<li><a href="Linear_context-free_rewriting_system" class="mw-redirect" title="Linear context-free rewriting system">Linear context-free rewriting systems</a></li>

<li><a href="Tree-adjoining_grammar" title="Tree-adjoining grammar">Tree-adjoining</a></li>

<li><a href="Context-free_grammar" title="Context-free grammar">Context-free</a></li>

<li><a href="Deterministic_context-free_grammar" title="Deterministic context-free grammar">Deterministic context-free</a></li>

<li><a href="Nested_word" title="Nested word">Visibly pushdown</a></li>

<li><a href="Regular_grammar" title="Regular grammar">Regular</a></li>

<li><a href="Non-recursive_grammar" class="mw-redirect" title="Non-recursive grammar">Non-recursive</a></li></ul>

</div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;width:10em;"><div>

<ul><li><a href="Recursively_enumerable_language" title="Recursively enumerable language">Recursively enumerable</a></li>

<li><a href="Recursive_language" title="Recursive language">Decidable</a></li>

<li><a href="Context-sensitive_language" title="Context-sensitive language">Context-sensitive</a></li>

<li>Positive <a href="Range_concatenation_language" class="mw-redirect" title="Range concatenation language">range concatenation</a>*</li>

<li><a href="Indexed_language" title="Indexed language">Indexed</a>*</li>

<li><a href="Linear_context-free_rewriting_language" class="mw-redirect" title="Linear context-free rewriting language">Linear context-free rewriting language</a></li>

<li><a href="Tree-adjoining_grammar" title="Tree-adjoining grammar">Tree-adjoining</a></li>

<li><a href="Context-free_language" title="Context-free language">Context-free</a></li>

<li><a href="Deterministic_context-free_language" title="Deterministic context-free language">Deterministic context-free</a></li>

<li><a href="Nested_word" title="Nested word">Visibly pushdown</a></li>

<li><a href="Regular_language" title="Regular language">Regular</a></li>

<li><a href="Finite_language" class="mw-redirect" title="Finite language">Finite</a></li></ul>

</div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;width:10em;"><div>

<ul><li><a href="Turing_machine" title="Turing machine">Turing machine</a></li>

<li><a href="Decider_(Turing_machine)" title="Decider (Turing machine)">Decider</a></li>

<li><a href="Linear_bounded_automaton" title="Linear bounded automaton">Linear-bounded</a></li>

<li><a href="PTIME" class="mw-redirect" title="PTIME">PTIME</a> Turing Machine</li>

<li><a href="Nested_stack_automaton" title="Nested stack automaton">Nested stack</a></li>

<li><a href="Thread_automaton" title="Thread automaton">Thread automaton</a></li>

<li>restricted <a href="Tree_stack_automaton" title="Tree stack automaton">Tree stack automaton</a></li>

<li><a href="Embedded_pushdown_automaton" title="Embedded pushdown automaton">Embedded pushdown</a></li>

<li><a href="Pushdown_automaton" title="Pushdown automaton">Nondeterministic pushdown</a></li>

<li><a href="Deterministic_pushdown_automaton" title="Deterministic pushdown automaton">Deterministic pushdown</a></li>

<li><a href="Nested_word" title="Nested word">Visibly pushdown</a></li>

<li><a href="Finite-state_machine" title="Finite-state machine">Finite</a></li>

<li><a href="Aperiodic_finite_state_automaton" class="mw-redirect" title="Aperiodic finite state automaton">Counter-free (with aperiodic finite monoid)</a></li>

<li><a href="Deterministic_acyclic_finite_state_automaton" title="Deterministic acyclic finite state automaton">Acyclic finite</a></li></ul>

</div></td></tr></tbody></table></div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div>Each category of languages, except those marked by a *, is a <a href="Proper_subset" class="mw-redirect" title="Proper subset">proper subset</a> of the category directly above it. Any language in each category is generated by a grammar and by an automaton in the category in the same line.</div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-07-09" href="https://en.wikipedia.org/wiki/?title=Tree_automaton&oldid=1299594829">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>